0 Prolog
↳1 PrologToPiTRSProof (⇒, 0 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 77 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 30 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 PiDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 PiDP
↳17 PiDPToQDPProof (⇒, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
↳21 PiDP
↳22 PiDPToQDPProof (⇒, 0 ms)
↳23 QDP
↳24 QDPOrderProof (⇔, 133 ms)
↳25 QDP
↳26 QDPOrderProof (⇔, 103 ms)
↳27 QDP
↳28 DependencyGraphProof (⇔, 0 ms)
↳29 QDP
↳30 UsableRulesProof (⇔, 0 ms)
↳31 QDP
↳32 QReductionProof (⇔, 0 ms)
↳33 QDP
↳34 UsableRulesReductionPairsProof (⇔, 0 ms)
↳35 QDP
↳36 PisEmptyProof (⇔, 0 ms)
↳37 YES
p_in_g(.(X, [])) → p_out_g(.(X, []))
p_in_g(.(s(s(X)), .(Y, Xs))) → U1_g(X, Y, Xs, p_in_g(.(X, .(Y, Xs))))
p_in_g(.(0, Xs)) → U4_g(Xs, p_in_g(Xs))
U4_g(Xs, p_out_g(Xs)) → p_out_g(.(0, Xs))
U1_g(X, Y, Xs, p_out_g(.(X, .(Y, Xs)))) → U2_g(X, Y, Xs, mult_in_gga(X, Y, Z))
mult_in_gga(X1, 0, 0) → mult_out_gga(X1, 0, 0)
mult_in_gga(X, s(Y), Z) → U6_gga(X, Y, Z, mult_in_gga(X, Y, W))
U6_gga(X, Y, Z, mult_out_gga(X, Y, W)) → U7_gga(X, Y, Z, sum_in_gga(W, X, Z))
sum_in_gga(X, 0, X) → sum_out_gga(X, 0, X)
sum_in_gga(X, s(Y), s(Z)) → U5_gga(X, Y, Z, sum_in_gga(X, Y, Z))
U5_gga(X, Y, Z, sum_out_gga(X, Y, Z)) → sum_out_gga(X, s(Y), s(Z))
U7_gga(X, Y, Z, sum_out_gga(W, X, Z)) → mult_out_gga(X, s(Y), Z)
U2_g(X, Y, Xs, mult_out_gga(X, Y, Z)) → U3_g(X, Y, Xs, p_in_g(.(Z, Xs)))
U3_g(X, Y, Xs, p_out_g(.(Z, Xs))) → p_out_g(.(s(s(X)), .(Y, Xs)))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
p_in_g(.(X, [])) → p_out_g(.(X, []))
p_in_g(.(s(s(X)), .(Y, Xs))) → U1_g(X, Y, Xs, p_in_g(.(X, .(Y, Xs))))
p_in_g(.(0, Xs)) → U4_g(Xs, p_in_g(Xs))
U4_g(Xs, p_out_g(Xs)) → p_out_g(.(0, Xs))
U1_g(X, Y, Xs, p_out_g(.(X, .(Y, Xs)))) → U2_g(X, Y, Xs, mult_in_gga(X, Y, Z))
mult_in_gga(X1, 0, 0) → mult_out_gga(X1, 0, 0)
mult_in_gga(X, s(Y), Z) → U6_gga(X, Y, Z, mult_in_gga(X, Y, W))
U6_gga(X, Y, Z, mult_out_gga(X, Y, W)) → U7_gga(X, Y, Z, sum_in_gga(W, X, Z))
sum_in_gga(X, 0, X) → sum_out_gga(X, 0, X)
sum_in_gga(X, s(Y), s(Z)) → U5_gga(X, Y, Z, sum_in_gga(X, Y, Z))
U5_gga(X, Y, Z, sum_out_gga(X, Y, Z)) → sum_out_gga(X, s(Y), s(Z))
U7_gga(X, Y, Z, sum_out_gga(W, X, Z)) → mult_out_gga(X, s(Y), Z)
U2_g(X, Y, Xs, mult_out_gga(X, Y, Z)) → U3_g(X, Y, Xs, p_in_g(.(Z, Xs)))
U3_g(X, Y, Xs, p_out_g(.(Z, Xs))) → p_out_g(.(s(s(X)), .(Y, Xs)))
P_IN_G(.(s(s(X)), .(Y, Xs))) → U1_G(X, Y, Xs, p_in_g(.(X, .(Y, Xs))))
P_IN_G(.(s(s(X)), .(Y, Xs))) → P_IN_G(.(X, .(Y, Xs)))
P_IN_G(.(0, Xs)) → U4_G(Xs, p_in_g(Xs))
P_IN_G(.(0, Xs)) → P_IN_G(Xs)
U1_G(X, Y, Xs, p_out_g(.(X, .(Y, Xs)))) → U2_G(X, Y, Xs, mult_in_gga(X, Y, Z))
U1_G(X, Y, Xs, p_out_g(.(X, .(Y, Xs)))) → MULT_IN_GGA(X, Y, Z)
MULT_IN_GGA(X, s(Y), Z) → U6_GGA(X, Y, Z, mult_in_gga(X, Y, W))
MULT_IN_GGA(X, s(Y), Z) → MULT_IN_GGA(X, Y, W)
U6_GGA(X, Y, Z, mult_out_gga(X, Y, W)) → U7_GGA(X, Y, Z, sum_in_gga(W, X, Z))
U6_GGA(X, Y, Z, mult_out_gga(X, Y, W)) → SUM_IN_GGA(W, X, Z)
SUM_IN_GGA(X, s(Y), s(Z)) → U5_GGA(X, Y, Z, sum_in_gga(X, Y, Z))
SUM_IN_GGA(X, s(Y), s(Z)) → SUM_IN_GGA(X, Y, Z)
U2_G(X, Y, Xs, mult_out_gga(X, Y, Z)) → U3_G(X, Y, Xs, p_in_g(.(Z, Xs)))
U2_G(X, Y, Xs, mult_out_gga(X, Y, Z)) → P_IN_G(.(Z, Xs))
p_in_g(.(X, [])) → p_out_g(.(X, []))
p_in_g(.(s(s(X)), .(Y, Xs))) → U1_g(X, Y, Xs, p_in_g(.(X, .(Y, Xs))))
p_in_g(.(0, Xs)) → U4_g(Xs, p_in_g(Xs))
U4_g(Xs, p_out_g(Xs)) → p_out_g(.(0, Xs))
U1_g(X, Y, Xs, p_out_g(.(X, .(Y, Xs)))) → U2_g(X, Y, Xs, mult_in_gga(X, Y, Z))
mult_in_gga(X1, 0, 0) → mult_out_gga(X1, 0, 0)
mult_in_gga(X, s(Y), Z) → U6_gga(X, Y, Z, mult_in_gga(X, Y, W))
U6_gga(X, Y, Z, mult_out_gga(X, Y, W)) → U7_gga(X, Y, Z, sum_in_gga(W, X, Z))
sum_in_gga(X, 0, X) → sum_out_gga(X, 0, X)
sum_in_gga(X, s(Y), s(Z)) → U5_gga(X, Y, Z, sum_in_gga(X, Y, Z))
U5_gga(X, Y, Z, sum_out_gga(X, Y, Z)) → sum_out_gga(X, s(Y), s(Z))
U7_gga(X, Y, Z, sum_out_gga(W, X, Z)) → mult_out_gga(X, s(Y), Z)
U2_g(X, Y, Xs, mult_out_gga(X, Y, Z)) → U3_g(X, Y, Xs, p_in_g(.(Z, Xs)))
U3_g(X, Y, Xs, p_out_g(.(Z, Xs))) → p_out_g(.(s(s(X)), .(Y, Xs)))
P_IN_G(.(s(s(X)), .(Y, Xs))) → U1_G(X, Y, Xs, p_in_g(.(X, .(Y, Xs))))
P_IN_G(.(s(s(X)), .(Y, Xs))) → P_IN_G(.(X, .(Y, Xs)))
P_IN_G(.(0, Xs)) → U4_G(Xs, p_in_g(Xs))
P_IN_G(.(0, Xs)) → P_IN_G(Xs)
U1_G(X, Y, Xs, p_out_g(.(X, .(Y, Xs)))) → U2_G(X, Y, Xs, mult_in_gga(X, Y, Z))
U1_G(X, Y, Xs, p_out_g(.(X, .(Y, Xs)))) → MULT_IN_GGA(X, Y, Z)
MULT_IN_GGA(X, s(Y), Z) → U6_GGA(X, Y, Z, mult_in_gga(X, Y, W))
MULT_IN_GGA(X, s(Y), Z) → MULT_IN_GGA(X, Y, W)
U6_GGA(X, Y, Z, mult_out_gga(X, Y, W)) → U7_GGA(X, Y, Z, sum_in_gga(W, X, Z))
U6_GGA(X, Y, Z, mult_out_gga(X, Y, W)) → SUM_IN_GGA(W, X, Z)
SUM_IN_GGA(X, s(Y), s(Z)) → U5_GGA(X, Y, Z, sum_in_gga(X, Y, Z))
SUM_IN_GGA(X, s(Y), s(Z)) → SUM_IN_GGA(X, Y, Z)
U2_G(X, Y, Xs, mult_out_gga(X, Y, Z)) → U3_G(X, Y, Xs, p_in_g(.(Z, Xs)))
U2_G(X, Y, Xs, mult_out_gga(X, Y, Z)) → P_IN_G(.(Z, Xs))
p_in_g(.(X, [])) → p_out_g(.(X, []))
p_in_g(.(s(s(X)), .(Y, Xs))) → U1_g(X, Y, Xs, p_in_g(.(X, .(Y, Xs))))
p_in_g(.(0, Xs)) → U4_g(Xs, p_in_g(Xs))
U4_g(Xs, p_out_g(Xs)) → p_out_g(.(0, Xs))
U1_g(X, Y, Xs, p_out_g(.(X, .(Y, Xs)))) → U2_g(X, Y, Xs, mult_in_gga(X, Y, Z))
mult_in_gga(X1, 0, 0) → mult_out_gga(X1, 0, 0)
mult_in_gga(X, s(Y), Z) → U6_gga(X, Y, Z, mult_in_gga(X, Y, W))
U6_gga(X, Y, Z, mult_out_gga(X, Y, W)) → U7_gga(X, Y, Z, sum_in_gga(W, X, Z))
sum_in_gga(X, 0, X) → sum_out_gga(X, 0, X)
sum_in_gga(X, s(Y), s(Z)) → U5_gga(X, Y, Z, sum_in_gga(X, Y, Z))
U5_gga(X, Y, Z, sum_out_gga(X, Y, Z)) → sum_out_gga(X, s(Y), s(Z))
U7_gga(X, Y, Z, sum_out_gga(W, X, Z)) → mult_out_gga(X, s(Y), Z)
U2_g(X, Y, Xs, mult_out_gga(X, Y, Z)) → U3_g(X, Y, Xs, p_in_g(.(Z, Xs)))
U3_g(X, Y, Xs, p_out_g(.(Z, Xs))) → p_out_g(.(s(s(X)), .(Y, Xs)))
SUM_IN_GGA(X, s(Y), s(Z)) → SUM_IN_GGA(X, Y, Z)
p_in_g(.(X, [])) → p_out_g(.(X, []))
p_in_g(.(s(s(X)), .(Y, Xs))) → U1_g(X, Y, Xs, p_in_g(.(X, .(Y, Xs))))
p_in_g(.(0, Xs)) → U4_g(Xs, p_in_g(Xs))
U4_g(Xs, p_out_g(Xs)) → p_out_g(.(0, Xs))
U1_g(X, Y, Xs, p_out_g(.(X, .(Y, Xs)))) → U2_g(X, Y, Xs, mult_in_gga(X, Y, Z))
mult_in_gga(X1, 0, 0) → mult_out_gga(X1, 0, 0)
mult_in_gga(X, s(Y), Z) → U6_gga(X, Y, Z, mult_in_gga(X, Y, W))
U6_gga(X, Y, Z, mult_out_gga(X, Y, W)) → U7_gga(X, Y, Z, sum_in_gga(W, X, Z))
sum_in_gga(X, 0, X) → sum_out_gga(X, 0, X)
sum_in_gga(X, s(Y), s(Z)) → U5_gga(X, Y, Z, sum_in_gga(X, Y, Z))
U5_gga(X, Y, Z, sum_out_gga(X, Y, Z)) → sum_out_gga(X, s(Y), s(Z))
U7_gga(X, Y, Z, sum_out_gga(W, X, Z)) → mult_out_gga(X, s(Y), Z)
U2_g(X, Y, Xs, mult_out_gga(X, Y, Z)) → U3_g(X, Y, Xs, p_in_g(.(Z, Xs)))
U3_g(X, Y, Xs, p_out_g(.(Z, Xs))) → p_out_g(.(s(s(X)), .(Y, Xs)))
SUM_IN_GGA(X, s(Y), s(Z)) → SUM_IN_GGA(X, Y, Z)
SUM_IN_GGA(X, s(Y)) → SUM_IN_GGA(X, Y)
From the DPs we obtained the following set of size-change graphs:
MULT_IN_GGA(X, s(Y), Z) → MULT_IN_GGA(X, Y, W)
p_in_g(.(X, [])) → p_out_g(.(X, []))
p_in_g(.(s(s(X)), .(Y, Xs))) → U1_g(X, Y, Xs, p_in_g(.(X, .(Y, Xs))))
p_in_g(.(0, Xs)) → U4_g(Xs, p_in_g(Xs))
U4_g(Xs, p_out_g(Xs)) → p_out_g(.(0, Xs))
U1_g(X, Y, Xs, p_out_g(.(X, .(Y, Xs)))) → U2_g(X, Y, Xs, mult_in_gga(X, Y, Z))
mult_in_gga(X1, 0, 0) → mult_out_gga(X1, 0, 0)
mult_in_gga(X, s(Y), Z) → U6_gga(X, Y, Z, mult_in_gga(X, Y, W))
U6_gga(X, Y, Z, mult_out_gga(X, Y, W)) → U7_gga(X, Y, Z, sum_in_gga(W, X, Z))
sum_in_gga(X, 0, X) → sum_out_gga(X, 0, X)
sum_in_gga(X, s(Y), s(Z)) → U5_gga(X, Y, Z, sum_in_gga(X, Y, Z))
U5_gga(X, Y, Z, sum_out_gga(X, Y, Z)) → sum_out_gga(X, s(Y), s(Z))
U7_gga(X, Y, Z, sum_out_gga(W, X, Z)) → mult_out_gga(X, s(Y), Z)
U2_g(X, Y, Xs, mult_out_gga(X, Y, Z)) → U3_g(X, Y, Xs, p_in_g(.(Z, Xs)))
U3_g(X, Y, Xs, p_out_g(.(Z, Xs))) → p_out_g(.(s(s(X)), .(Y, Xs)))
MULT_IN_GGA(X, s(Y), Z) → MULT_IN_GGA(X, Y, W)
MULT_IN_GGA(X, s(Y)) → MULT_IN_GGA(X, Y)
From the DPs we obtained the following set of size-change graphs:
U1_G(X, Y, Xs, p_out_g(.(X, .(Y, Xs)))) → U2_G(X, Y, Xs, mult_in_gga(X, Y, Z))
U2_G(X, Y, Xs, mult_out_gga(X, Y, Z)) → P_IN_G(.(Z, Xs))
P_IN_G(.(s(s(X)), .(Y, Xs))) → U1_G(X, Y, Xs, p_in_g(.(X, .(Y, Xs))))
P_IN_G(.(s(s(X)), .(Y, Xs))) → P_IN_G(.(X, .(Y, Xs)))
P_IN_G(.(0, Xs)) → P_IN_G(Xs)
p_in_g(.(X, [])) → p_out_g(.(X, []))
p_in_g(.(s(s(X)), .(Y, Xs))) → U1_g(X, Y, Xs, p_in_g(.(X, .(Y, Xs))))
p_in_g(.(0, Xs)) → U4_g(Xs, p_in_g(Xs))
U4_g(Xs, p_out_g(Xs)) → p_out_g(.(0, Xs))
U1_g(X, Y, Xs, p_out_g(.(X, .(Y, Xs)))) → U2_g(X, Y, Xs, mult_in_gga(X, Y, Z))
mult_in_gga(X1, 0, 0) → mult_out_gga(X1, 0, 0)
mult_in_gga(X, s(Y), Z) → U6_gga(X, Y, Z, mult_in_gga(X, Y, W))
U6_gga(X, Y, Z, mult_out_gga(X, Y, W)) → U7_gga(X, Y, Z, sum_in_gga(W, X, Z))
sum_in_gga(X, 0, X) → sum_out_gga(X, 0, X)
sum_in_gga(X, s(Y), s(Z)) → U5_gga(X, Y, Z, sum_in_gga(X, Y, Z))
U5_gga(X, Y, Z, sum_out_gga(X, Y, Z)) → sum_out_gga(X, s(Y), s(Z))
U7_gga(X, Y, Z, sum_out_gga(W, X, Z)) → mult_out_gga(X, s(Y), Z)
U2_g(X, Y, Xs, mult_out_gga(X, Y, Z)) → U3_g(X, Y, Xs, p_in_g(.(Z, Xs)))
U3_g(X, Y, Xs, p_out_g(.(Z, Xs))) → p_out_g(.(s(s(X)), .(Y, Xs)))
U1_G(X, Y, Xs, p_out_g) → U2_G(Xs, mult_in_gga(X, Y))
U2_G(Xs, mult_out_gga(Z)) → P_IN_G(.(Z, Xs))
P_IN_G(.(s(s(X)), .(Y, Xs))) → U1_G(X, Y, Xs, p_in_g(.(X, .(Y, Xs))))
P_IN_G(.(s(s(X)), .(Y, Xs))) → P_IN_G(.(X, .(Y, Xs)))
P_IN_G(.(0, Xs)) → P_IN_G(Xs)
p_in_g(.(X, [])) → p_out_g
p_in_g(.(s(s(X)), .(Y, Xs))) → U1_g(X, Y, Xs, p_in_g(.(X, .(Y, Xs))))
p_in_g(.(0, Xs)) → U4_g(p_in_g(Xs))
U4_g(p_out_g) → p_out_g
U1_g(X, Y, Xs, p_out_g) → U2_g(Xs, mult_in_gga(X, Y))
mult_in_gga(X1, 0) → mult_out_gga(0)
mult_in_gga(X, s(Y)) → U6_gga(X, mult_in_gga(X, Y))
U6_gga(X, mult_out_gga(W)) → U7_gga(sum_in_gga(W, X))
sum_in_gga(X, 0) → sum_out_gga(X)
sum_in_gga(X, s(Y)) → U5_gga(sum_in_gga(X, Y))
U5_gga(sum_out_gga(Z)) → sum_out_gga(s(Z))
U7_gga(sum_out_gga(Z)) → mult_out_gga(Z)
U2_g(Xs, mult_out_gga(Z)) → U3_g(p_in_g(.(Z, Xs)))
U3_g(p_out_g) → p_out_g
p_in_g(x0)
U4_g(x0)
U1_g(x0, x1, x2, x3)
mult_in_gga(x0, x1)
U6_gga(x0, x1)
sum_in_gga(x0, x1)
U5_gga(x0)
U7_gga(x0)
U2_g(x0, x1)
U3_g(x0)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
P_IN_G(.(0, Xs)) → P_IN_G(Xs)
POL(.(x1, x2)) = x1 + x2
POL(0) = 1
POL(P_IN_G(x1)) = x1
POL(U1_G(x1, x2, x3, x4)) = x2 + x3
POL(U1_g(x1, x2, x3, x4)) = 1
POL(U2_G(x1, x2)) = x1 + x2
POL(U2_g(x1, x2)) = 0
POL(U3_g(x1)) = 0
POL(U4_g(x1)) = 1
POL(U5_gga(x1)) = x1
POL(U6_gga(x1, x2)) = x2
POL(U7_gga(x1)) = x1
POL([]) = 0
POL(mult_in_gga(x1, x2)) = x2
POL(mult_out_gga(x1)) = x1
POL(p_in_g(x1)) = 1
POL(p_out_g) = 0
POL(s(x1)) = x1
POL(sum_in_gga(x1, x2)) = x1
POL(sum_out_gga(x1)) = x1
mult_in_gga(X1, 0) → mult_out_gga(0)
mult_in_gga(X, s(Y)) → U6_gga(X, mult_in_gga(X, Y))
U6_gga(X, mult_out_gga(W)) → U7_gga(sum_in_gga(W, X))
sum_in_gga(X, 0) → sum_out_gga(X)
sum_in_gga(X, s(Y)) → U5_gga(sum_in_gga(X, Y))
U7_gga(sum_out_gga(Z)) → mult_out_gga(Z)
U5_gga(sum_out_gga(Z)) → sum_out_gga(s(Z))
U1_G(X, Y, Xs, p_out_g) → U2_G(Xs, mult_in_gga(X, Y))
U2_G(Xs, mult_out_gga(Z)) → P_IN_G(.(Z, Xs))
P_IN_G(.(s(s(X)), .(Y, Xs))) → U1_G(X, Y, Xs, p_in_g(.(X, .(Y, Xs))))
P_IN_G(.(s(s(X)), .(Y, Xs))) → P_IN_G(.(X, .(Y, Xs)))
p_in_g(.(X, [])) → p_out_g
p_in_g(.(s(s(X)), .(Y, Xs))) → U1_g(X, Y, Xs, p_in_g(.(X, .(Y, Xs))))
p_in_g(.(0, Xs)) → U4_g(p_in_g(Xs))
U4_g(p_out_g) → p_out_g
U1_g(X, Y, Xs, p_out_g) → U2_g(Xs, mult_in_gga(X, Y))
mult_in_gga(X1, 0) → mult_out_gga(0)
mult_in_gga(X, s(Y)) → U6_gga(X, mult_in_gga(X, Y))
U6_gga(X, mult_out_gga(W)) → U7_gga(sum_in_gga(W, X))
sum_in_gga(X, 0) → sum_out_gga(X)
sum_in_gga(X, s(Y)) → U5_gga(sum_in_gga(X, Y))
U5_gga(sum_out_gga(Z)) → sum_out_gga(s(Z))
U7_gga(sum_out_gga(Z)) → mult_out_gga(Z)
U2_g(Xs, mult_out_gga(Z)) → U3_g(p_in_g(.(Z, Xs)))
U3_g(p_out_g) → p_out_g
p_in_g(x0)
U4_g(x0)
U1_g(x0, x1, x2, x3)
mult_in_gga(x0, x1)
U6_gga(x0, x1)
sum_in_gga(x0, x1)
U5_gga(x0)
U7_gga(x0)
U2_g(x0, x1)
U3_g(x0)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
P_IN_G(.(s(s(X)), .(Y, Xs))) → U1_G(X, Y, Xs, p_in_g(.(X, .(Y, Xs))))
POL(.(x1, x2)) = 1 + x2
POL(0) = 0
POL(P_IN_G(x1)) = x1
POL(U1_G(x1, x2, x3, x4)) = 1 + x3
POL(U1_g(x1, x2, x3, x4)) = 0
POL(U2_G(x1, x2)) = 1 + x1
POL(U2_g(x1, x2)) = 0
POL(U3_g(x1)) = 0
POL(U4_g(x1)) = 0
POL(U5_gga(x1)) = 0
POL(U6_gga(x1, x2)) = 0
POL(U7_gga(x1)) = 0
POL([]) = 0
POL(mult_in_gga(x1, x2)) = 0
POL(mult_out_gga(x1)) = 0
POL(p_in_g(x1)) = 0
POL(p_out_g) = 0
POL(s(x1)) = 0
POL(sum_in_gga(x1, x2)) = 0
POL(sum_out_gga(x1)) = 0
U1_G(X, Y, Xs, p_out_g) → U2_G(Xs, mult_in_gga(X, Y))
U2_G(Xs, mult_out_gga(Z)) → P_IN_G(.(Z, Xs))
P_IN_G(.(s(s(X)), .(Y, Xs))) → P_IN_G(.(X, .(Y, Xs)))
p_in_g(.(X, [])) → p_out_g
p_in_g(.(s(s(X)), .(Y, Xs))) → U1_g(X, Y, Xs, p_in_g(.(X, .(Y, Xs))))
p_in_g(.(0, Xs)) → U4_g(p_in_g(Xs))
U4_g(p_out_g) → p_out_g
U1_g(X, Y, Xs, p_out_g) → U2_g(Xs, mult_in_gga(X, Y))
mult_in_gga(X1, 0) → mult_out_gga(0)
mult_in_gga(X, s(Y)) → U6_gga(X, mult_in_gga(X, Y))
U6_gga(X, mult_out_gga(W)) → U7_gga(sum_in_gga(W, X))
sum_in_gga(X, 0) → sum_out_gga(X)
sum_in_gga(X, s(Y)) → U5_gga(sum_in_gga(X, Y))
U5_gga(sum_out_gga(Z)) → sum_out_gga(s(Z))
U7_gga(sum_out_gga(Z)) → mult_out_gga(Z)
U2_g(Xs, mult_out_gga(Z)) → U3_g(p_in_g(.(Z, Xs)))
U3_g(p_out_g) → p_out_g
p_in_g(x0)
U4_g(x0)
U1_g(x0, x1, x2, x3)
mult_in_gga(x0, x1)
U6_gga(x0, x1)
sum_in_gga(x0, x1)
U5_gga(x0)
U7_gga(x0)
U2_g(x0, x1)
U3_g(x0)
P_IN_G(.(s(s(X)), .(Y, Xs))) → P_IN_G(.(X, .(Y, Xs)))
p_in_g(.(X, [])) → p_out_g
p_in_g(.(s(s(X)), .(Y, Xs))) → U1_g(X, Y, Xs, p_in_g(.(X, .(Y, Xs))))
p_in_g(.(0, Xs)) → U4_g(p_in_g(Xs))
U4_g(p_out_g) → p_out_g
U1_g(X, Y, Xs, p_out_g) → U2_g(Xs, mult_in_gga(X, Y))
mult_in_gga(X1, 0) → mult_out_gga(0)
mult_in_gga(X, s(Y)) → U6_gga(X, mult_in_gga(X, Y))
U6_gga(X, mult_out_gga(W)) → U7_gga(sum_in_gga(W, X))
sum_in_gga(X, 0) → sum_out_gga(X)
sum_in_gga(X, s(Y)) → U5_gga(sum_in_gga(X, Y))
U5_gga(sum_out_gga(Z)) → sum_out_gga(s(Z))
U7_gga(sum_out_gga(Z)) → mult_out_gga(Z)
U2_g(Xs, mult_out_gga(Z)) → U3_g(p_in_g(.(Z, Xs)))
U3_g(p_out_g) → p_out_g
p_in_g(x0)
U4_g(x0)
U1_g(x0, x1, x2, x3)
mult_in_gga(x0, x1)
U6_gga(x0, x1)
sum_in_gga(x0, x1)
U5_gga(x0)
U7_gga(x0)
U2_g(x0, x1)
U3_g(x0)
P_IN_G(.(s(s(X)), .(Y, Xs))) → P_IN_G(.(X, .(Y, Xs)))
p_in_g(x0)
U4_g(x0)
U1_g(x0, x1, x2, x3)
mult_in_gga(x0, x1)
U6_gga(x0, x1)
sum_in_gga(x0, x1)
U5_gga(x0)
U7_gga(x0)
U2_g(x0, x1)
U3_g(x0)
p_in_g(x0)
U4_g(x0)
U1_g(x0, x1, x2, x3)
mult_in_gga(x0, x1)
U6_gga(x0, x1)
sum_in_gga(x0, x1)
U5_gga(x0)
U7_gga(x0)
U2_g(x0, x1)
U3_g(x0)
P_IN_G(.(s(s(X)), .(Y, Xs))) → P_IN_G(.(X, .(Y, Xs)))
No rules are removed from R.
P_IN_G(.(s(s(X)), .(Y, Xs))) → P_IN_G(.(X, .(Y, Xs)))
POL(.(x1, x2)) = 2·x1 + x2
POL(P_IN_G(x1)) = 2·x1
POL(s(x1)) = 2·x1